$\forall$$T$:Type, $P$:(($T$ List)$\rightarrow$$T$$\rightarrow$Prop).
\\[0ex]($\forall$$L$:$T$ List, $x$:$T$. Dec($P$($L$,$x$)))
\\[0ex]$\Rightarrow$ ($\forall$$L$:$T$ List. Dec($\exists$${\it L'}$:$T$ List, $x$:$T$. $L$ $=$ (${\it L'}$ @ [$x$]) \& $P$(${\it L'}$,$x$)))